es:ES, P1, P2:(E), Q1, R1, Q2, R2:(EE), f:({e:E| P1(e)} E).
P2  P1
 Q2 => Q1
 R1 => R2
 {f is Q1-R1-pre-preserving on P1  f is Q2-R2-pre-preserving on P2} 

latex

Definitions	x:A. B(x), , P  Q, t  T, {T}, x:A. B(x), x. t(x), S  T, suptype(S; T), P  Q, P1  P2, R1  R2, t  ...$L, R1 => R2, P1  P2, x(s)
Lemmas	rel implies wf, es-E wf, predicate implies wf, event system wf, Q-R-pre-preserving wf, subtype rel function, subtype rel set, Q-R-pre-preserving functionality wrt implies, rel implies weakening, rel equivalent weakening, rel equivalent inversion, predicate implies weakening, predicate equivalent weakening, predicate equivalent inversion